1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
/*!
Reduction to normal form
*/
use super::*;

/// A reduction configuration to keep going until reaching a given form for up to `n` compound reductions.
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub struct NormalCfg {
    /// The maximum number of steps which can be taken.
    pub max_steps: u64,
    /// Whether to perform eta reductions
    pub eta: bool,
    /// Whether to perform head beta reductions
    pub head: bool,
    /// Whether to perform non-head beta reductions
    pub sub: bool,
}

impl NormalCfg {
    /// Create a new normal configuration targeting a form with a given number of maximum steps
    pub fn to_form(form: Form, max_steps: u64) -> NormalCfg {
        NormalCfg {
            max_steps,
            eta: form.is_enf(),
            head: form.is_hnf(),
            sub: form.is_bnf() || form.is_enf(),
        }
    }
}

impl ReductionConfig for NormalCfg {
    type AsRef = NormalCfg;

    #[inline]
    fn register_push_subst(&mut self, _subst: &TermId) -> Result<(), Error> {
        Ok(())
    }

    #[inline]
    fn register_pop_subst(&mut self) -> Result<(), Error> {
        Ok(())
    }

    #[inline]
    fn register_beta(&mut self) -> Result<(), Error> {
        if self.max_steps == 0 {
            return Err(Error::StopReduction);
        }
        self.max_steps -= 1;
        Ok(())
    }

    #[inline]
    fn register_eta(&mut self) -> Result<(), Error> {
        if self.max_steps == 0 {
            return Err(Error::StopReduction);
        }
        self.max_steps -= 1;
        Ok(())
    }

    #[inline]
    fn eta(&self, _term: &Term, _ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
        if self.max_steps == 0 {
            return Err(Error::StopReduction);
        } else {
            Ok(self.eta)
        }
    }

    #[inline]
    fn sub(&self, _term: &Term, _ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
        if self.max_steps == 0 {
            return Err(Error::StopReduction);
        } else {
            Ok(self.sub)
        }
    }

    #[inline]
    fn head(&self, _term: &Term, _ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
        if self.max_steps == 0 {
            return Err(Error::StopReduction);
        } else {
            Ok(self.head)
        }
    }

    #[inline]
    fn intersects(&self, _filter: VarFilter, _code: Code, form: Form) -> bool {
        (self.head && !form.is_hnf())
            || (self.sub && !((self.head && form.is_bnf()) && (self.eta && form.is_enf())))
            || (self.eta && !form.is_enf())
    }

    #[inline]
    fn as_ref_mut(&mut self) -> &mut Self::AsRef {
        self
    }
}